Skip to content

Instantly share code, notes, and snippets.

Definition sig_fst {A B} {p q : {x : A | B x}} (H : p = q)
: proj1_sig p = proj1_sig q :=
eq_rect _ (fun z => proj1_sig p = proj1_sig z) eq_refl _ H.
Definition sig_snd {A B} {p q : {x : A | B x}} (H : p = q)
: eq_rect _ B (proj2_sig p) _ (sig_fst H) = proj2_sig q :=
match H with
| eq_refl => eq_refl
end.

Self Types for better languages

This post intends to promote self types as a safer, simpler, and faster alternative to inductive types and dependent pattern matching at the core of programming languages.

In summary, it should go through the problems that self types try to solve, the problems that they introduce, and then a concrete solution proposed at the end, with a syntax-directed, bidirectional type system with decidable checking.

SYNTAX at the Syntax section.

The problem

@steveruizok
steveruizok / SKILL.md
Created July 25, 2026 20:10
/bikeshed
name bikeshed
description Run two independent subagents through a structured debate on the same prompt — independent answers, cross-critique, revision, then a synthesized unified response. Use when explicitly invoked as /bikeshed with a prompt, or when the user asks for a two-agent debate/adversarial comparison on a plan, design, or other complex piece of work. Best for plans and complex open-ended work, not simple factual questions.

Bikeshed: two-agent structured debate

Take the user's prompt (everything after /bikeshed), run it through two independent subagents in a debate protocol, and synthesize their final answers into one unified response. If no prompt was given, ask the user what question or plan to bikeshed before starting.

The value comes from independence followed by controlled exchange. Do not let either agent see the other's work before Round 1 is complete, and do not editorialize when relaying material between them — pass responses and critiques verbatim.

@conradcaffier03
conradcaffier03 / glm-5-2-free-setup.md
Last active July 26, 2026 00:52
GLM-5.2 Free Setup Guide — the genuinely free ways to run Z.ai GLM-5.2 (chat + free API), plus the paid Claude Code path

GLM-5.2 Free Setup Guide

GLM-5.2 is Z.ai's open-weights (MIT) flagship — 744B-MoE, a 1M-token context, and benchmarks within ~1 point of Claude Opus 4.8 on FrontierSWE. Here's how to actually put it to work, starting with the routes that cost nothing and need no credit card.


1. Free, zero setup — just chat

#!/bin/bash
TIMESTORE="/var/lib/avc-audit-report.last-run"
TMPFILE=`mktemp /tmp/avc-audit-report.XXXXXXXXXX`
if [ -e "$TIMESTORE" ]; then
LASTRUN=`cat ${TIMESTORE}`
else
LASTRUN="yesterday"
fi
@mricon
mricon / wtftz.sh
Last active July 26, 2026 00:42
Quick timezone chart
#!/bin/bash
WANT=$1
dotime () {
WANT=$1
PAC=`TZ='America/Vancouver' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"`
MTN=`TZ='America/Denver' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"`
CEN=`TZ='America/Chicago' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"`
UTC=`TZ='Etc/UTC' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"`
CST=`TZ='Asia/Shanghai' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"`
@mricon
mricon / snaplock-prep.sh
Created December 10, 2012 15:18
Using syslog with snaplock
#!/bin/bash
SNAPLOCK="/mnt/snaplock"
for ZONE in internal dmz frontend; do
YESTERDAY=`date +'%Y/%m/%d' -d 'yesterday'`
TOMORROW=`date +'%Y/%m/%d' -d 'tomorrow'`
LOCKTILL=`date +'%Y%m%d0000' -d '+5 years'`
if [ -d "${SNAPLOCK}/${ZONE}/${YESTERDAY}" ]; then
@mricon
mricon / mysnaplock.te
Created December 10, 2012 15:49
Allow cron to do the necessary operation on mounted var_log_t from cron
module mysnaplock 1.0.0;
require {
type cron_log_t;
type var_log_t;
class filesystem associate;
}
#============= cron_log_t ==============
allow cron_log_t var_log_t:filesystem associate;
#!/bin/bash
# Downtimes are third Sunday of the month. In order to plan
# for upgrades and reboots, we email ourselves the list of all
# outstanding security updates for each system on the 2nd
# Wednesday of the month.
# Critical security update alerts are sent daily.
# Requires yum-plugin-security and mailx.
WEEKOFMONTH=$((($(date +%d)-1)/7+1))
DAYOFWEEK=$(date +%u)
@mricon
mricon / keybase.md
Created September 25, 2014 14:57
keybase.md

Keybase proof

I hereby claim:

  • I am mricon on github.
  • I am mricon (https://keybase.io/mricon) on keybase.
  • I have a public key whose fingerprint is DE0E 66E3 2F1F DD09 0266 6B96 E63E DCA9 329D D07E

To claim this, I am signing this object: